Inference at * 
Iof proof for Lemma can-apply-compose':


  A, B, C:Type, g:(A(B + Top)), f:(ABC), x:A. can-apply(f o' g;x) ~ can-apply(g;x) 

latex

 by ((((UnivCD) 
CollapseTHENA (Auto))) 
CCollapseTHEN (((RepUR ``do-apply can-apply p-compose\'
CC`` ( 0)) 
CCollapseTHEN (((((GenConclAtAddr [1;1;1;1]) 
CollapseTHENA (Auto))) 
CCollapseTHEN (
CC((D (-2)) 
CCollapseTHEN (((Reduce 0) 
CCollapseTHEN (Auto)))))))))) 

latex

CC.

Definitions	s ~ t, f o' g, can-apply(f;x), do-apply(f;x), P  Q, f(a), Type, Top, x:A. B(x), x:AB(x), t  T, s = t, left + right
Lemmas	top wf